BackThruLemma `assert\_of\_ff`